+ Quot.surjective_mk
+ Quotient.coe_smul_out
+ Quotient.hrecOn_mk
+ Quotient.hrecOn₂_mk
+ Quotient.mk_smul_out
+ Quotient.surjective_liftOn
+ Quotient.surjective_mk
+ Quotient.surjective_mk'
+ _root_.QuotientGroup.out_conj_pow_minimalPeriod_mem
+ acc_liftOn₂_iff
+ decidableRel
+ equiv_iff_apply
+ ext'_iff
+ instance (q : Quotient sa) (f : α → Prop) (h : ∀ a b, sa a b → f a = f b) [DecidablePred f] :
+ instance : CoeFun (Setoid α) (fun _ ↦ α → α → Prop)
+ instance : Inhabited (ValueGroup A K) := ⟨⟦0⟧⟩
+ instance : One (HomogeneousLocalization 𝒜 x) where one := ⟦1⟧
+ instance : One (ValueGroup A K) := ⟨⟦1⟧⟩
+ instance : Zero (HomogeneousLocalization 𝒜 x) where zero := ⟦0⟧
+ instance : Zero (ValueGroup A K) := ⟨⟦0⟧⟩
+ instance [r : Setoid α] [h : DecidableRel (α := α) (· ≈ ·)] : DecidableRel r
+ instance {α : Type*} (s : Setoid α) : IsEquiv α s
+ measurable_quotient_mk
+ quotMk_eq_coe
+ range_quotient_liftOn
++ out_eq
+-+- mk
+-+- mk_surjective
+--+ map
+--- out_eq'
- Setoid.decidableRel
- ext_iff
- instance (q : Quotient sa) (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [DecidablePred f] :
- instance (q : Quotient s₁) (f : α → Prop) (h : ∀ a b, @Setoid.r α s₁ a b → f a = f b)
- instance (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → Prop)
- instance : Inhabited (ValueGroup A K) := ⟨Quotient.mk'' 0⟩
- instance : One (HomogeneousLocalization 𝒜 x) where one := Quotient.mk'' 1
- instance : One (ValueGroup A K) := ⟨Quotient.mk'' 1⟩
- instance : Zero (HomogeneousLocalization 𝒜 x) where zero := Quotient.mk'' 0
- instance : Zero (ValueGroup A K) := ⟨Quotient.mk'' 0⟩
-+-+ mk''_eq_mk
--++ stabilizerEquivStabilizerOfOrbitRel
--- argument.

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.